\begin{tabbing}
$\forall$$T$:Type, ${\it as}$:($T$ List), $f$,$g$:($T$$\rightarrow\mathbb{B}$).
\\[0ex]subtype\_rel($T$; $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ sorted(${\it as}$)
\\[0ex]$\Rightarrow$ \=((priority{-}select($f$; $g$; ${\it as}$) = (inl ff ) $\in$ (?$\mathbb{B}$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ l\_exists(${\it as}$; $T$; $a$.(($\uparrow$($g$($a$))) $\wedge$ ($\forall$$b$:$T$. ($b$ $\in$ ${\it as}$) $\Rightarrow$ ($b$ $\leq$ $a$) $\Rightarrow$ ($\neg$($\uparrow$($f$($b$))))))))
\-
\end{tabbing}